$\forall$$T$:Type, $n$:$\mathbb{N}$, $f$:(int\_seg(0; $n$)$\rightarrow$$T$). $\parallel$mklist($n$; $f$)$\parallel$ = $n$ $\in$ $\mathbb{Z}$